Nuprl Lemma : l_all_iff
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
P
:(
T
). (
x
L
.
P
(
x
))
(
i
:{0..||
L
||
}.
P
(
L
[
i
]))
latex
Definitions
Type
,
t
T
,
s
=
t
,
type
List
,
,
x
:
A
B
(
x
)
,
||
as
||
,
a
<
b
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
,
{
x
:
A
|
B
(
x
)}
,
{
i
..
j
}
,
Void
,
x
:
A
.
B
(
x
)
,
l
[
i
]
,
f
(
a
)
,
x
(
s
)
,
#$n
,
,
|
g
|
,
S
T
,
A
c
B
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
(
x
l
)
,
x
L
.
P
(
x
)
Lemmas
le
wf
,
nat
wf
,
int
seg
wf
,
length
wf1
,
select
wf
origin
T:Type, L:(T List), P:(T
). (x
L. P(x)) 
(i:{0..||L||
}. P(L[i])) T:Type, L:(T List), P:(T). (xL. P(x)) (i:{0..||L||}. P(L[i])) TB(x) Q
A
B j < k
}x:A. B(x)
T
B
B(x)
x:A. B(x) Q Q l)xL. P(x)